Skip to content

Fix docs push - #217

Closed
mrjackv wants to merge 1 commit into
revng:developfrom
mrjackv:feature/fix-docs-push
Closed

mrjackv wants to merge 1 commit into
revng:developfrom
mrjackv:feature/fix-docs-push

Conversation

@mrjackv

@mrjackv mrjackv commented Sep 10, 2026

Copy link
Copy Markdown
Contributor

No description provided.

The docs ssh key is encoded in base64, decode it before feeding it to
`ssh-add`.
@aleclearmind

Copy link
Copy Markdown
Contributor

Merged in 7d6cf12. Thanks.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants